es:event_system{i:l}, e:es-E(es), l:IdLnk, L:(es-E(es) List).
es-rcv-from(es; e; l; L)  (i:int_seg(0; ||L||). es-index(es; L[i]) = i  ) 

latex

Definitions

||as||, , b, x:A  B(x), x:A. B(x), P  Q, False, A, P  Q, A  B, lelt(i; j; k), , {x:A| B(x)} , int_seg(i; j), x:A. B(x), a < b, #$n, t  T, void, x:AB(x), es-eq(es), eqof(d), f(a), x.A(x), mu(f), prop{i:l}, es_info(es), Id, True, T, event_system{i:l}, IdLnk, A c B, P  Q, es-rcv-from(es; e; l; L), index(dE; dL; pred?; info; p; r), es-index(es; e), l[i], es-lnk(es; e), es-sender(es; e), es-receives(es; e; l), es-E(es), type List, s = t, no_repeats(T; l), l_before(x; y; l; T), P  Q, es-locl(es; e; e'), Type

Lemmas

eqof equal btrue, assert wf, mu-bound, le wf, no repeats mu index, es-locl wf, es-locl-antireflexive, no repeats iff, l before wf, int seg wf, es-rcv-from wf, es-rcv-from-equal-receives, select member, es-receives wf, squash wf, true wf, IdLnk wf, event system wf, rcv?-link, rcv?-kind, Id wf, es info wf, mu wf, eqof wf, es-eq wf, select wf, nat wf, length wf1, es-E wf